Termination Proof Script
Consider the TRS R consisting of the rewrite rules
|
| 1: |
|
rec(rec(x)) |
→ sent(rec(x)) |
| 2: |
|
rec(sent(x)) |
→ sent(rec(x)) |
| 3: |
|
rec(no(x)) |
→ sent(rec(x)) |
| 4: |
|
rec(bot) |
→ up(sent(bot)) |
| 5: |
|
rec(up(x)) |
→ up(rec(x)) |
| 6: |
|
sent(up(x)) |
→ up(sent(x)) |
| 7: |
|
no(up(x)) |
→ up(no(x)) |
| 8: |
|
top(rec(up(x))) |
→ top(check(rec(x))) |
| 9: |
|
top(sent(up(x))) |
→ top(check(rec(x))) |
| 10: |
|
top(no(up(x))) |
→ top(check(rec(x))) |
| 11: |
|
check(up(x)) |
→ up(check(x)) |
| 12: |
|
check(sent(x)) |
→ sent(check(x)) |
| 13: |
|
check(rec(x)) |
→ rec(check(x)) |
| 14: |
|
check(no(x)) |
→ no(check(x)) |
| 15: |
|
check(no(x)) |
→ no(x) |
|
There are 25 dependency pairs:
|
| 16: |
|
REC(rec(x)) |
→ SENT(rec(x)) |
| 17: |
|
REC(sent(x)) |
→ SENT(rec(x)) |
| 18: |
|
REC(sent(x)) |
→ REC(x) |
| 19: |
|
REC(no(x)) |
→ SENT(rec(x)) |
| 20: |
|
REC(no(x)) |
→ REC(x) |
| 21: |
|
REC(bot) |
→ SENT(bot) |
| 22: |
|
REC(up(x)) |
→ REC(x) |
| 23: |
|
SENT(up(x)) |
→ SENT(x) |
| 24: |
|
NO(up(x)) |
→ NO(x) |
| 25: |
|
TOP(rec(up(x))) |
→ TOP(check(rec(x))) |
| 26: |
|
TOP(rec(up(x))) |
→ CHECK(rec(x)) |
| 27: |
|
TOP(rec(up(x))) |
→ REC(x) |
| 28: |
|
TOP(sent(up(x))) |
→ TOP(check(rec(x))) |
| 29: |
|
TOP(sent(up(x))) |
→ CHECK(rec(x)) |
| 30: |
|
TOP(sent(up(x))) |
→ REC(x) |
| 31: |
|
TOP(no(up(x))) |
→ TOP(check(rec(x))) |
| 32: |
|
TOP(no(up(x))) |
→ CHECK(rec(x)) |
| 33: |
|
TOP(no(up(x))) |
→ REC(x) |
| 34: |
|
CHECK(up(x)) |
→ CHECK(x) |
| 35: |
|
CHECK(sent(x)) |
→ SENT(check(x)) |
| 36: |
|
CHECK(sent(x)) |
→ CHECK(x) |
| 37: |
|
CHECK(rec(x)) |
→ REC(check(x)) |
| 38: |
|
CHECK(rec(x)) |
→ CHECK(x) |
| 39: |
|
CHECK(no(x)) |
→ NO(check(x)) |
| 40: |
|
CHECK(no(x)) |
→ CHECK(x) |
|
The approximated dependency graph contains 5 SCCs:
{24},
{23},
{18,20,22},
{34,36,38,40}
and {25,28,31}.
-
Consider the SCC {24}.
There are no usable rules.
By taking the AF π with
π(NO) = 1 together with
the lexicographic path order with
empty precedence,
rule 24
is strictly decreasing.
-
Consider the SCC {23}.
There are no usable rules.
By taking the AF π with
π(SENT) = 1 together with
the lexicographic path order with
empty precedence,
rule 23
is strictly decreasing.
-
Consider the SCC {18,20,22}.
There are no usable rules.
By taking the AF π with
π(no) = π(REC) = π(sent) = 1 together with
the lexicographic path order with
empty precedence,
the rules in {18,20}
are weakly decreasing and
rule 22
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {18,20}.
By taking the AF π with
π(no) = π(REC) = 1 together with
the lexicographic path order with
empty precedence,
rule 20
is weakly decreasing and
rule 18
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {20}.
By taking the AF π with
π(REC) = 1 together with
the lexicographic path order with
empty precedence,
rule 20
is strictly decreasing.
-
Consider the SCC {34,36,38,40}.
There are no usable rules.
By taking the AF π with
π(CHECK) = π(no) = π(rec) = π(sent) = 1 together with
the lexicographic path order with
empty precedence,
the rules in {36,38,40}
are weakly decreasing and
rule 34
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {36,38,40}.
By taking the AF π with
π(CHECK) = π(no) = π(rec) = 1 together with
the lexicographic path order with
empty precedence,
the rules in {38,40}
are weakly decreasing and
rule 36
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {38,40}.
By taking the AF π with
π(CHECK) = π(no) = 1 together with
the lexicographic path order with
empty precedence,
rule 40
is weakly decreasing and
rule 38
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {40}.
By taking the AF π with
π(CHECK) = 1 together with
the lexicographic path order with
empty precedence,
rule 40
is strictly decreasing.
-
Consider the SCC {25,28,31}.
The usable rules are {1-7,11-15}.
By taking the AF π with
π(check) = π(sent) = π(TOP) = 1
and π(no) = π(rec) = π(up) = [ ] together with
the lexicographic path order with
precedence no ≻ up
and up ≈ rec,
the rules in {1-6,11-15,25,28}
are weakly decreasing and
the rules in {7,31}
are strictly decreasing.
There is one new SCC.
-
Consider the SCC {25,28}.
By taking the AF π with
π(check) = π(no) = π(sent) = π(TOP) = 1 together with
the lexicographic path order with
precedence up ≈ rec,
the rules in {2-7,11-15,28}
are weakly decreasing and
the rules in {1,25}
are strictly decreasing.
There is one new SCC.
-
Consider the SCC {28}.
The constraints could not be solved.
Tyrolean Termination Tool (0.32 seconds)
--- May 4, 2006